Resolution and cut-free LK are the most popular propositional systems used for logical automated reasoning. The question whether or not resolution and cut-free LK have the same efficiency on the system of CNF formulas has been asked and studied since 1960 425–467). It was shown in Cook and Reckhow, J. Symbolic Logic 44 36–50 that tree resolution has super-polynomial speed-up over cut-free LK. Naturally, the current issue is whether or not resolution and cut-free LK expressed as directed acyclic graphs have (...) the same efficiency. In this paper, we introduce a new algorithm to eliminate atomic cuts and show that cut-free LK polynomially simulates resolution when the input formula is expressed as a k-CNF formula. As a corollary, we show that regular resolution does not polynomially simulate cut-free LK . We also show that cut-free LK polynomially simulates regular resolution. (shrink)

The method of analytic tableaux is employed in many introductory texts and has also been used quite extensively as a basis for automated theorem proving. In this paper, we discuss the complexity of the system as a method for refuting contradictory sets of clauses, and resolve several open questions. We discuss the three forms of analytic tableaux: clausal tableaux, generalized clausal tableaux, and binary tableaux. We resolve the relative complexity of these three forms of tableaux proofs and also resolve the (...) relative complexity of analytic tableaux versus resolution. We show that there is a quasi-polynomial simulation of tree resolution by analytic tableaux; this simulation is close to optimal, since we give a matching lower bound that is tight to within a polynomial. (shrink)

Hilbert proposed the epsilon substitution method as a basis for consistency proofs. Hilbert's Ansatz for finding a solving substitution for any given finite set of transfinite axioms is, starting with the null substitution S0, to correct false values step by step and thereby generate the process S0,S1,… . The problem is to show that the approximating process terminates. After Gentzen's innovation, Ackermann 162) succeeded to prove termination of the process for first order arithmetic. Inspired by G. Mints as an Ariadne's (...) thread we formulate the epsilon substitution method for the theory ID1 of non-iterated inductive definitions for disjunctions of simply universal and existential operators, and give a termination proof of the H-process based on Ackermann 162). The termination proof is based on transfinite induction up to the Howard ordinal. (shrink)

We formulate epsilon substitution method for theories (H)α0 of absolute jump hierarchies, and give two termination proofs of the H-process: The first proof is an adaption of Mints M, Mints-Tupailo-Buchholz MTB, i.e., based on a cut-elimination of a specially devised infinitary calculus. The second one is an adaption of Ackermann Ack. Each termination proof is based on transfinite induction up to an ordinal θ(α0+ ω)0, which is best possible.

For α < ε0, Nα denotes the number of occurrences of ω in the Cantor normal form of α with the base ω. For a binary number-theoretic function f let B denote the length n of the longest descending chain of ordinals <ε0 such that for all i < n, Nαi ≤ f . Simpson [2] called ε0 as slowly well ordered when B is totally defined for f = K · . Let |n| denote the binary length of the (...) natural number n, and |n|k the k-times iterate of the logarithmic function |n|. For a unary function h let L denote the function B ) with h0 = K + |i| · |i|h. In this note we show, inspired from Weiermann [4], that, under a reasonable condition on h, the functionL is primitive recursive in the inverse h–1 and vice versa. (shrink)

An assessment of mood or emotion is important in developing mental health measures, and facial expressions are strongly related to mood or emotion. This study thus aimed to examine the relationship between levels of negative mood and characteristics of mouth parts when moods are drawn as facial expressions on a common platform. A cross-sectional study of Japanese college freshmen was conducted, and 1,068 valid responses were analyzed. The questionnaire survey consisted of participants’ characteristics, the Profile of Mood States, and a (...) sheet of facial expression drawing, and the sheet was digitized and analyzed using an image-analysis software. Based on the total POMS score as an index of negative mood, the participants were divided into four groups: low, normal, high, and very high. Lengths of drawn lines and between both mouth corners were significantly longer, and circularity and roundness were significantly higher in the L group. With increasing levels of negative mood, significant decreasing trends were observed in these lengths. Convex downward and enclosed figures were significantly predominant in the L group, while convex upward figures were significantly predominant and a tendency toward predominance of no drawn mouths or line figures was found in the H and VH groups. Our results suggest that mood states can be significantly related to the size and figure characteristics of drawn mouths of FACED on a non-verbal common platform. That is, these findings mean that subjects with low negative mood may draw a greater and rounder mouth and figures that may be enclosed and downward convex, while subjects with a high negative mood may not draw the line, or if any, may draw the line shorter and upward convex. (shrink)

Let H be a proof system for quantified propositional calculus (QPC). We define the Σqj-witnessing problem for H to be: given a prenex Σqj-formula A, an H-proof of A, and a truth assignment to the free variables in A, find a witness for the outermost existential quantifiers in A. We point out that the Σq1-witnessing problems for the systems G*1and G1 are complete for polynomial time and PLS (polynomial local search), respectively. We introduce and study the systems G*0 and G0, (...) in which cuts are restricted to quantifier-free formulas, and prove that the Σqj-witnessing problem for each is complete for NC1. Our proof involves proving a polynomial time version of Gentzen’s midsequent theorem for G*0 and proving that G0-proofs are TC0-recognizable. We also introduce QPC systems for TC0 and prove witnessing theorems for them. We introduce a finitely axiomatizable second-order system VNC1 of bounded arithmetic which we prove isomorphic to Arai’s first order theory AID + Σb0-CA for uniform NC1. We describe simple translations of VNC1 proofs of all bounded theorems to polynomial size families of G*0 proofs. From this and the above theorem we get alternative proofs of the NC1 witnessing theorems for VNC1 and AID. (shrink)

This research examines the current status of clinical ethics consultation (CEC) in Japan through a nationwide study conducted with chairs of ethics committees and clinical ethics committees among 1028 post-graduate clinical teaching hospitals. We also qualitatively analyzed their viewpoints of the CEC’s benefits and problems related to hospital consultation services to identify the critical points for CEC and inform the development of a correctly functioning system. The questionnaire included structured questions about hospital CEC organization and service purpose and operation and (...) open-ended questions about the benefits and problems of initiating CEC. The questionnaire comprised the presence/absence of an ethics committee, CEC services and membership when services were implemented, users, and the number of cases handled since inception. In addition, the respondents also provided their impressions of the CEC system’s impact on their hospital by describing (a) the benefits of CEC services and (b) the ineffectual or harmful aspects of the CEC system. Qualitative data were examined using qualitative content analysis to determine the impact of establishing a CEC and the difficulties of practice. One hundred twenty-five questionnaires were returned from either the chair of the ethics committee or clinical ethics committee in teaching hospitals. Of these, 90 (72%) reported they provided CEC services. Additionally, 36 respondents (34.6%) reported that their existing research and clinical ethics committees had conducted CEC services, and 35 (33.7%) reported having a newly established clinical ethics committee conducting CEC services. Three positive effects of establishing and four challenges in managing CEC were also identified. (shrink)

This paper deals with a proof theory for a theory T22 of recursively Mahlo ordinals in the form of Π2-reflecting on Π2-reflecting ordinals using a subsystem Od of the system O of ordinal diagrams in Arai 353). This paper is the first published one in which a proof-theoretic analysis à la Gentzen–Takeuti of recursively large ordinals is expounded.

This paper deals with a proof theory for a theory T3 of Π3-reflecting ordinals using the system O of ordinal diagrams in Arai 1375). This is a sequel to the previous one 1) in which a theory for recursively Mahlo ordinals is analyzed proof-theoretically.

BackgroundFew comparative studies of clinical ethics consultation practices have been reported. The objective of this study was to explore how American and Japanese experts analyze an Alzheimer's case regarding ethics consultation.MethodsWe presented the case to physicians and ethicists from the US and Japan (one expert from each field from both countries; total = 4) and obtained their responses through a questionnaire and in-depth interviews.ResultsEstablishing a consensus was a common goal among American and Japanese participants. In attempting to achieve consensus, the (...) most significant similarity between Japanese and American ethics consultants was that they both appeared to adopt an "ethics facilitation" approach. Differences were found in recommendation and assessment between the American and Japanese participants. In selecting a surrogate, the American participants chose to contact the grandson before designating the daughter-in-law as the surrogate decision-maker. Conversely the Japanese experts assumed that the daughter-in-law was the surrogate.ConclusionOur findings suggest that consensus building through an "ethics facilitation" approach may be a commonality to the practice of ethics consultation in the US and Japan, while differences emerged in terms of recommendations, surrogate assessment, and assessing treatments. Further research is needed to appreciate differences not only among different nations including, but not limited to, countries in Europe, Asia and the Americas, but also within each country. (shrink)

Healthcare professionals must make decisions for patients based on ethical considerations. However, they rely on clinical ethics consultations (CEC) to review ethical justifications of their decisions. CEC consultants support the cases reviewed and guide medical care. When both healthcare professionals and CEC consultants face ethical problems in medical care, how is their judgment derived? How do medical judgments differ from the ethical considerations of CECs? This study examines CECs in Japan to identify differences in the ethical judgment of clients and (...) CEC consultants. (shrink)

In this, journal, W. Buchholz gave an elegant proof of a characterization theorem for provably total recursive functions in the theory IDv for the v-times iterated inductive definitions . He characterizes the classes of functions by Hardy functions. In this note we will show that a slow growing analogue to the theorem can be obtained by a slight modification of Buchholz' proof.

We gather the following miscellaneous results in proof theory from the attic.1. 1. A provably well-founded elementary ordering admits an elementary order preserving map.2. 2. A simple proof of an elementary bound for cut elimination in propositional calculus and its applications to separation problem in relativized bounded arithmetic below S21.3. 3. Equivalents for Bar Induction, e.g., reflection schema for ω logic.4. 4. Direct computations in an equational calculus PRE and a decidability problem for provable inequations in PRE.5. 5. Intuitionistic fixed (...) point theories which are conservative extensions of HA.6. 6. Proof theoretic strengths of classical fixed points theories.7. 7. An equivalence between transfinite induction rule and iterated reflection schema over IΣn.8. 8. Derivation lengths of finite rewrite rules reducing under lexicographic path orders and multiply recursive functions.Each section can be read separately in principle. (shrink)

Background There are several psychosocial and ethical issues surrounding the decision to be a living kidney donor. The present study aimed to determine the perceptions of psychosocial and ethical issues that living kidney donors may have, and analyze their psychological characteristics.Methods Face-to-face semi-structured interviews were conducted with 15 donors. Thematic analysis was then performed to categorize the thematic elements of the transcripts. All procedures were approved by the relevant review board.Results Four main categories were identified: Awareness of family dynamics, barriers (...) to a proper understanding, contrasting psychological effects of recipient presence in clinical practice, insufficient information explained in informed consent.Conclusion Donors felt that they took on the “role as a care giver” for the recipient and were less aware of themselves as patients. This is a new concept that has not been shown in previous studies. Donors exist within the recipient and family, and the range of their autonomy may go beyond the traditional concept of autonomy and be rooted in relational autonomy. This study suggested that medical treatment in the presence of the recipient promotes the relational autonomy of the donor. (shrink)

In Arai (An ordinal analysis of a single stable ordinal, submitted) it is shown that an ordinal \(\sup _{N is an upper bound for the proof-theoretic ordinal of a set theory \(\mathsf {KP}\ell ^{r}+(M\prec _{\Sigma _{1}}V)\). In this paper we show that a second order arithmetic \(\Sigma ^{1-}_{2}{\mathrm {-CA}}+\Pi ^{1}_{1}{\mathrm {-CA}}_{0}\) proves the wellfoundedness up to \(\psi _{\varOmega _{1}}(\varepsilon _{\varOmega _{{\mathbb {S}}+N+1}})\) for each _N_. It is easy to interpret \(\Sigma ^{1-}_{2}{\mathrm {-CA}}+\Pi ^{1}_{1}{\mathrm {-CA}}_{0}\) in \(\mathsf {KP}\ell ^{r}+(M\prec _{\Sigma (...) _{1}}V)\). (shrink)

In this note the well-ordering principle for the derivative \ of normal functions \ on ordinals is shown to be equivalent to the existence of arbitrarily large countable coded \-models of the well-ordering principle for the function \.

In this paper we introduce a recursive notation system $O(\mu)$ of ordinals. An element of the notation system is called an ordinal diagram following G. Takeuti [25]. The system is designed for proof theoretic study of theories of recursively Mahlo universes. We show that for each $\alpha<\Omega$ in $O(\mu)$ KPM proves that the initial segment of $O(\mu)$ determined by $\alpha$ is a well ordering. Proof theoretic study for such theories will be reported in [9].

In this paper, we prove the wellfoundedness of recursive notation systems for reflecting ordinals up to Π₃-reflection by relevant inductive definitions.

In the circular sphere around the Pacific Ocean many volcanos have erupted, and, because of tectonic plates, numerous earthquakes have occurred. In Tonga, especially, the resulting devastation has been beyond our wildest imagination. Regarding such natural phenomena, we could not predict anything. Likewise, the Covid-19 pandemic appeared suddenly, and no one can say when its destruction will end. Protective measures against infection have affected the nature of our social interactions: masking has changed our spatial consciousness; observing social distancing has made (...) us less dependent on one another and has influenced us to seek solitude. As a result, inter-subjectivity—the foundation of ethics—has been broken. All of these effects on our interpersonal relationships have instilled in us a new attitude towards nature, because the human being is a part of nature. This new attitude with nature opens up a new paradigm: dialogues with nature and their co-operative activities must be demanded, and we must wait for nature’s movement and ask for its help. It is, in a way, the traditional artistic attitude toward nature. (shrink)

Avec et après la pandémie, notre conscience de l’espace et du temps a subi un changement radical : les individus ont expérimenté l’oisiveté forcée, les gestes barrières et la distanciation physique qui redouble l’éloignement induit par les nouvelles technologies ayant substitué la communication à l’échange. Or, les progrès techniques n’ont de progrès que le nom et ne cherchent que l’efficacité assurée par la vitesse qui fait violence aux cycles de la nature. Pourtant, seule cette dernière est capable de nous réconcilier (...) avec nous-mêmes en nous extrayant de la domination de la machine et en nous enseignant la patience de laquelle peut surgir la beauté : beauté du geste artistique qui défie le temps, accès à la transcendance à travers la contemplation du vivant. C’est dans ce rapport d’interdépendance avec la nature que nous pouvons échapper à la déshumanisation de la société moderne et renouer avec la beauté du monde. (shrink)

In the case of Japan, we accepted the Chinese philosophy of morality when we received the Chinese character Yi: it means responsibility to Heaven (vertical) and, at the same time, responsibility to community (horizontal). An act having this structure might be our responsibility as human beings: yi means “justice”, keeping balance between Heaven and Earth. The Japanese people had such a balance until the Edo era. In 1868, when the Meiji Restoration occurred, the Japanese government tried to accept Western ideas. (...) Cyoumin Nakae introduced the Western philosophy of law and the constitutional system. He translated Rousseau’s The Social Contract into Japanese and gave a series of lectures on the social contract. The fundament of his thought is concentrated in the “rights of Liberty”. He emphasized transcendental liberty beyond personal, phenomenal liberty and found the same structure in Mencius. His idea of ft suggests the way of justice. Unfortunately, this idea was crushed with the death of his talented disciple in prison. After the book of Bushido, ft was only translated as “duty” for the community (horizontal), and we lost the vertical perspective: transcendental liberty. (shrink)

Inspired by earthquakes in the world, I attempt to clarify the relationship between human beings and Nature. Many architects, such as Tange and Isozaki from 1963 until 2005, built modern cities under the idea of urbanism. However, in Eco-ethica, we propose a new concept “urbanica.” It suggests a new relationship—not “city-center and suburbs” but free relations among communities. New relationships must be clarified in ethics. I try to make clear the relationship between inter-subjectivity and inter-objectivity. I analyze this through a (...) Noh play, “Yamanba,” which is a symbol of one natural phenomenon, “wind”: a personified figure of “wind” should link inter-subjectivity and inter-objectivity. Nature itself makes reality, the real world, by the potential movement of wind. (shrink)

The Pragmatics of Multi-Verb Sequences: The Case of the Verb Go This paper is an empirical investigation into the nature of multi-verb sequences in English. Multi-verb sequences such as V-to-VP and V-and-VP present a natural construction type of investigating recurring patterns of event sequences as conceived situations. This paper focuses on the image-schematic properties of both the go-to-VP construction and the go-and-VP construction to which previous accounts have paid little attention, and it demonstrates that the interpretation of the image-schemas has (...) enhanced research. The go-to-VP and the go-and-VP constructions require different image schemas. With respect to the go-to-VP construction, the SOURCE-PATH-GOAL schema plays an important role; sometimes a compound image schema of that type are necessary. Specifically, the image-schematic properties of the first verb go are incorporated into the event structure of the second verb to allow the speaker to construe the event denoted by the second verb in accordance with the image-schematic meaning of the first verb go. Consequently, this paper offers a pragmatic and cognitive account of the two constructions respectively. Some results in a data-driven analysis in this paper also reinforce selected convincing explanations. (shrink)

The mechanism of chromosome condensation is one of the classic mysteries of mitosis. A number of years ago, it was suggested that nonhistone proteins of the chromosome scaffold fraction might help chromosomes to condense, possibly by constructing a framework for the condensed structure. Recent results have shown that topoisomerase II and the SMC proteins, two abundant members of the scaffold fraction, are required for chromosome condensation and segregation during mitosis. Topoisomerase II is a well‐characterized enzyme. In contrast, nothing is yet (...) known about the function of the SMC proteins. We summarize evidence suggesting that these proteins may be enzymes whose activity is somehow involved in the establishment and maintenance of mitotic chromosome morphology. (shrink)

In this paper we introduce a recursive notation system O(Π 3 ) of ordinals. An element of the notation system is called an ordinal diagram. The system is designed for proof theoretic study of theories of Π 3 -reflection. We show that for each $\alpha in O(Π 3 ) a set theory KP Π 3 for Π 3 -reflection proves that the initial segment of O(Π 3 ) determined by α is a well ordering. Proof theoretic study for such theories (...) will be reported in [4]. (shrink)

We show that the existence of a weakly compact cardinal over the Zermelo–Fraenkel's set theory ZF is proof-theoretically reducible to iterations of Mostowski collapsings and Mahlo operations.